1  /-
  2  Copyright (c) 2019 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro
  5  -/
  6  import data.rat.order
src         └────────────┘
  7  /-!
  8  # Casts for Rational Numbers
  9  
 10  ## Summary
 11  
 12  We define the canonical injection from ℚ into an arbitrary division ring and prove various
 13  casting lemmas showing the well-behavedness of this injection.
 14  
 15  ## Notations
 16  
 17  - `/.` is infix notation for `rat.mk`.
 18  
 19  ## Tags
 20  
 21  rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting
 22  -/
 23  
 24  namespace rat
 25  variable {α : Type*}
id            
typ           
 26  open_locale rat
 27  
 28  section with_div_ring
 29  variable [division_ring α]
id             └───────────┘
src            └───────────┘
typ            └───────────┘
 30  
 31  /-- Construct the canonical injection from `ℚ` into an arbitrary
 32    division ring. If the field has positive characteristic `p`,
 33    we define `1 / p = 1 / 0 = 0` for consistency with our
 34    division by zero convention. -/
 35  protected def cast : ℚ → α
id                          
src                        
typ                         
doc                       
 36  | ⟨n, d, h, c⟩ := n / d
id                └┘   
src                 └┘   
typ               └┘   
 37  
 38  @[priority 10] instance cast_coe : has_coe ℚ α := ⟨rat.cast⟩
id                                      └─────┘       └──────┘
src                                     └─────┘        └──────┘
typ                                     └─────┘       └──────┘
doc                                                    └──────┘
 39  
 40  @[simp] theorem cast_of_int (n : ℤ) : (of_int n : α) = n :=
id                                         └────┘       
src                                        └────┘        
typ                                        └────┘       
doc    └──┘                                 └────┘
 41  show (n / (1:ℕ) : α) = n, by rw [nat.cast_one, div_one]
id                              └──────────┘  └─────┘
src                            └──┘└──────────┘└┘└─────┘└─
typ                         └──┘└──────────┘└┘└─────┘└─
doc                               └──┘            └┘       └─
txt                               └──┘            └┘       └─
par                               └──┘            └┘       └─
pid                                 └┘            └┘       
st                               └───────────────┘└───────┘
 42  
src  
typ  
doc  
txt  
par  
pid  
st   
 43  @[simp, squash_cast] theorem cast_coe_int (n : ℤ) : ((n : ℚ) : α) = n :=
id                                                                  
src                                                                  
typ                                                                 
doc    └──┘  └─────────┘                                       
 44  by rw [coe_int_eq_of_int, cast_of_int]
id          └───────────────┘  └─────────┘
src     └──┘└───────────────┘└┘└─────────┘└─
typ     └──┘└───────────────┘└┘└─────────┘└─
doc     └──┘                 └┘           └─
txt     └──┘                 └┘           └─
par     └──┘                 └┘           └─
pid       └┘                 └┘           
st     └────────────────────┘└───────────┘
 45  
src  
typ  
doc  
txt  
par  
pid  
st   
 46  @[simp, squash_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℚ) : α) = n := cast_coe_int n
id                                                                      └──────────┘ 
src                                                                        └──────────┘
typ                                                                     └──────────┘ 
doc    └──┘  └─────────┘                                       
 47  
 48  @[simp, squash_cast] theorem cast_zero : ((0 : ℚ) : α) = 0 :=
id                                                        
src                                                        
typ                                                       
doc    └──┘  └─────────┘                            
 49  (cast_of_int _).trans int.cast_zero
id    └─────────┘   └───┘  └───────────┘
src   └─────────┘   └───┘  └───────────┘
typ   └─────────┘   └───┘  └───────────┘
 50  
 51  @[simp, squash_cast] theorem cast_one : ((1 : ℚ) : α) = 1 :=
id                                                       
src                                                       
typ                                                      
doc    └──┘  └─────────┘                           
 52  (cast_of_int _).trans int.cast_one
id    └─────────┘   └───┘  └──────────┘
src   └─────────┘   └───┘  └──────────┘
typ   └─────────┘   └───┘  └──────────┘
 53  
 54  theorem mul_cast_comm (a : α) :
id                              
typ                             
 55    ∀ (n : ℚ), (n.denom : α) ≠ 0 → a * n = n * a
id               └────┘                
src                └────┘                   
typ              └────┘                
doc           
 56  | ⟨n, d, h, c⟩ h₂ := show a * (n * d⁻¹) = n * d⁻¹ * a,
id                                  └┘       └┘  
src                                    └┘       └┘ 
typ                                 └┘       └┘  
 57    by rw [← mul_assoc, int.mul_cast_comm, mul_assoc, mul_assoc,
id              └───────┘  └───────────────┘  └───────┘  └───────┘
src       └────┘└───────┘└┘└───────────────┘└┘└───────┘└┘└───────┘└─
typ       └────┘└───────┘└┘└───────────────┘└┘└───────┘└┘└───────┘└─
doc       └────┘         └┘                 └┘         └┘         └─
txt       └────┘         └┘                 └┘         └┘         └─
par       └────┘         └┘                 └┘         └┘         └─
pid         └──┘         └┘                 └┘         └┘         └─
st       └──────────────┘└─────────────────┘└─────────┘└─────────┘└─
 58           ← show (d:α)⁻¹ * a = a * d⁻¹, from
id                       └┘    
src  ──────────┘       └┘      └──────
typ  ──────────┘      └┘      └──────
doc  ──────────┘                 └──────
txt  ──────────┘                 └──────
par  ──────────┘                 └──────
pid  ──────────┘                 └──────
st   ────────────────────────────────────────────
 59             division_ring.inv_comm_of_comm h₂ (int.mul_cast_comm a d).symm]
id              └────────────────────────────┘ └┘  └───────────────┘  
src  ──────────┘└────────────────────────────┘   └───────────────┘  └───────
typ  ──────────┘└────────────────────────────┘└┘ └───────────────┘└───────
doc  ──────────┘                                                    └───────
txt  ──────────┘                                                    └───────
par  ──────────┘                                                    └───────
pid  ──────────┘                                                    └─────┘
st   ───────────────────────────────────────────────────────────────────────┘└┘
 60  
src  
typ  
doc  
txt  
par  
pid  
st   
 61  @[move_cast] theorem cast_mk_of_ne_zero (a b : ℤ)
id                                                  
src                                                 
typ                                                 
doc    └───────┘
 62    (b0 : (b:α) ≠ 0) : (a /. b : α) = a / b :=
id                       └┘         
src                         └┘           
typ                      └┘         
doc                          └┘
 63  begin
st   └─────
 64    have b0' : b ≠ 0, { refine mt _ b0, simp {contextual := tt} },
id                              └┘   └┘                      └┘
src    └─────────┘ └┘    └─────┘└┘└─┘    └───┘ └────────────┘└┘└┘
typ    └─────────┘└┘    └─────┘└┘└─┘└┘  └───┘ └────────────┘└┘└┘
doc    └─────────┘  └┘    └─────┘  └─┘    └───┘ └────────────┘  └┘
txt    └─────────┘  └┘    └─────┘  └─┘    └───┘ └────────────┘  └┘
par    └─────────┘  └┘    └─────┘  └─┘    └───┘ └────────────┘  └┘
pid    └──────┘└─┘              └─┘         └────────────┘  
st   ─────────────────┘└──┘└────────────┘└────────────────────────┘└┘
 65    cases e : a /. b with n d h c,
id                   
src    └────┘ └─┘    └───────────┘
typ    └────┘ └─┘  └───────────┘
doc    └────┘ └─┘    └───────────┘
txt    └────┘ └─┘    └───────────┘
par    └────┘ └─┘    └───────────┘
pid          └─┘    └───────────┘
st   ──────────────────────────────┘└─
 66    have d0 : (d:α) ≠ 0,
id                 
src    └────────┘   └┘ └┘
typ    └────────┘ └┘ └┘
doc    └────────┘   └┘ └┘
txt    └────────┘   └┘ └┘
par    └────────┘   └┘ └┘
pid    └─────┘└─┘   └┘ 
st   ────────────────────┘└─
 67    { intro d0,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid           └─┘
st   ───┘└──────┘└─
 68      have dd := denom_dvd a b,
id                  └───────┘  
src      └─────────┘└───────┘ 
typ      └─────────┘└───────┘
doc      └─────────┘          
txt      └─────────┘          
par      └─────────┘          
pid      └─────┘└─┘          
st   ───────────────────────────┘└─
 69      cases (show (d:ℤ) ∣ b, by rwa e at dd) with k ke,
id                                  
src      └────┘        └┘ └───┘└──┘ └────┘└─────────┘
typ      └────┘       └┘└───┘└──┘└────┘└─────────┘
doc      └────┘        └┘  └───┘└──┘ └────┘└─────────┘
txt      └────┘        └┘  └───┘└──┘ └────┘└─────────┘
par      └────┘        └┘  └───┘└──┘ └────┘└─────────┘
pid                   └┘  └───────┘ └─────┘└────────┘
st   ────────────────────────────┘└──────────┘└─────────┘└─
 70      have : (b:α) = (d:α) * (k:α), {rw [ke, int.cast_mul], refl},
id                                     └┘  └──────────┘
src      └─────┘   └┘    └┘      └──┘  └┘└──────────┘  └──┘
typ      └─────┘  └┘   └┘    └──┘└┘└┘└──────────┘  └──┘
doc      └─────┘   └┘    └┘       └──┘  └┘              └──┘
txt      └─────┘   └┘    └┘       └──┘  └┘              └──┘
par      └─────┘   └┘    └┘       └──┘  └┘              └──┘
pid      └───┘└┘   └┘    └┘         └┘  └┘            
st   ───────────────────────────────┘└─────┘└┘└────────────┘└─────┘└┘
 71      rw [d0, zero_mul] at this, contradiction },
id           └┘  └──────┘
src      └──┘  └┘└──────┘└───────┘  └────────────┘
typ      └──┘└┘└┘└──────┘└───────┘  └────────────┘
doc      └──┘  └┘        └───────┘  └────────────┘
txt      └──┘  └┘        └───────┘  └────────────┘
par      └──┘  └┘        └───────┘  └────────────┘
pid        └┘  └┘        └──────┘               
st   ─────────┘└────────┘└──────┘└──────────────┘└┘
 72    rw [num_denom'] at e,
id         └────────┘
src    └──┘└────────┘└────┘
typ    └──┘└────────┘└────┘
doc    └──┘          └────┘
txt    └──┘          └────┘
par    └──┘          └────┘
pid      └┘          └───┘
st   ───────────────┘└───┘└─
 73    have := congr_arg (coe : ℤ → α) ((mk_eq b0' $ ne_of_gt $ int.coe_nat_pos.2 h).1 e),
id             └───────┘  └─┘           └───┘ └─┘   └──────┘   └─────────────┘       
src    └──────┘└───────┘ └─┘└─┘   └┘  └───┘    └──────┘ └─────────────┘└─┘ └──┘ 
typ    └──────┘└───────┘ └─┘└─┘  └┘  └───┘└─┘ └──────┘ └─────────────┘└─┘└──┘
doc    └──────┘             └─┘   └┘                                   └─┘ └──┘ 
txt    └──────┘             └─┘   └┘                                   └─┘ └──┘ 
par    └──────┘             └─┘   └┘                                   └─┘ └──┘ 
pid    └───┘└─┘             └─┘   └┘                                   └─┘ └──┘ 
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
 74    rw [int.cast_mul, int.cast_mul, int.cast_coe_nat] at this,
id         └──────────┘  └──────────┘  └──────────────┘
src    └──┘└──────────┘└┘└──────────┘└┘└──────────────┘└───────┘
typ    └──┘└──────────┘└┘└──────────┘└┘└──────────────┘└───────┘
doc    └──┘            └┘            └┘                └───────┘
txt    └──┘            └┘            └┘                └───────┘
par    └──┘            └┘            └┘                └───────┘
pid      └┘            └┘            └┘                └──────┘
st   ─────────────────┘└────────────┘└────────────────┘└──────┘└─
 75    symmetry, change (a * b⁻¹ : α) = n / d,
id                          └┘         
src    └──────┘  └─────┘    └┘└─┘ └┘  
typ    └──────┘  └─────┘  └┘└─┘└┘ 
doc    └──────┘  └─────┘      └─┘ └┘   
txt    └──────┘  └─────┘      └─┘ └┘   
par    └──────┘  └─────┘      └─┘ └┘   
pid                          └─┘ └┘   
st   ─────────┘└────────────────────────────┘└─
 76    rw [eq_div_iff_mul_eq _ _ d0, mul_assoc, nat.mul_cast_comm,
id         └───────────────┘     └┘  └───────┘  └───────────────┘
src    └──┘└───────────────┘└───┘  └┘└───────┘└┘└───────────────┘└─
typ    └──┘└───────────────┘└───┘└┘└┘└───────┘└┘└───────────────┘└─
doc    └──┘                 └───┘  └┘         └┘                 └─
txt    └──┘                 └───┘  └┘         └┘                 └─
par    └──┘                 └───┘  └┘         └┘                 └─
pid      └┘                 └───┘  └┘         └┘                 └─
st   ─────────────────────────────┘└─────────┘└─────────────────┘└─
 77        ← mul_assoc, this, mul_assoc, mul_inv_cancel b0, mul_one]
id           └───────┘  └──┘  └───────┘  └────────────┘ └┘  └─────┘
src  ───────┘└───────┘└┘    └┘└───────┘└┘└────────────┘  └┘└─────┘└┘
typ  ───────┘└───────┘└┘└──┘└┘└───────┘└┘└────────────┘└┘└┘└─────┘└┘
doc  ───────┘         └┘    └┘         └┘                └┘       └┘
txt  ───────┘         └┘    └┘         └┘                └┘       └┘
par  ───────┘         └┘    └┘         └┘                └┘       └┘
pid  ───────┘         └┘    └┘         └┘                └┘       
st   ────────────────┘└────┘└─────────┘└─────────────────┘└───────┘
 78  end
st   └─┘
 79  
 80  @[move_cast] theorem cast_add_of_ne_zero : ∀ {m n : ℚ},
id                                                      
src                                                      
typ                                                     
doc    └───────┘                                         
 81    (m.denom : α) ≠ 0 → (n.denom : α) ≠ 0 → ((m + n : ℚ) : α) = m + n
id      └────┘           └────┘                          
src      └────┘             └────┘                              
typ     └────┘           └────┘                          
doc                                                      
 82  | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := λ (d₁0 : (d₁:α) ≠ 0) (d₂0 : (d₂:α) ≠ 0), begin
id          └┘               └┘                                             
src                                                                           
typ         └┘               └┘                                             
st                                                                                   └─────
 83    have d₁0' : (d₁:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d₁0; exact d₁0 rfl),
id                  └┘         └─────────────────┘                              └─┘ └─┘
src    └──────────┘   └┘└────┘└─────────────────┘└─┘  └──┘  └─┘ └─────┘└┘└────┘   └─┘
typ    └──────────┘ └┘└┘└────┘└─────────────────┘└─┘  └──┘  └─┘└─────┘└┘└────┘└─┘└─┘
doc    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
txt    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
par    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
pid    └───────┘└─┘    └┘ └───┘                   └─┘  └──┘  └──┘ └─────────────┘      
st   ─────────────────────────────────────────────────────────┘└─────────────────────────┘└─
 84    have d₂0' : (d₂:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d₂0; exact d₂0 rfl),
id                  └┘           └─────────────────┘                              └─┘ └─┘
src    └──────────┘    └┘ └────┘└─────────────────┘└─┘  └──┘  └─┘ └─────┘└┘└────┘   └─┘
typ    └──────────┘ └┘ └┘ └────┘└─────────────────┘└─┘  └──┘  └─┘└─────┘└┘└────┘└─┘└─┘
doc    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
txt    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
par    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
pid    └───────┘└─┘    └┘ └───┘                   └─┘  └──┘  └──┘ └─────────────┘      
st   ─────────────────────────────────────────────────────────┘└─────────────────────────┘└─
 85    rw [num_denom', num_denom', add_def d₁0' d₂0'],
id         └────────┘  └────────┘  └─────┘ └──┘ └──┘
src    └──┘└────────┘└┘└────────┘└┘└─────┘        
typ    └──┘└────────┘└┘└────────┘└┘└─────┘└──┘└──┘
doc    └──┘          └┘          └┘               
txt    └──┘          └┘          └┘               
par    └──┘          └┘          └┘               
pid      └┘          └┘          └┘               
st   ───────────────┘└──────────┘└─────────────────┘└──
 86    suffices : (n₁ * (d₂ * (d₂⁻¹ * d₁⁻¹)) +
id                              └┘          
src    └─────────┘          └┘     └─┘
typ    └─────────┘          └┘     └─┘
doc    └─────────┘                  └─┘ 
txt    └─────────┘                  └─┘ 
par    └─────────┘                  └─┘ 
pid    └───────┘└┘                  └─┘ 
st   ──────────────────────────────────────────
 87      n₂ * (d₁ * d₂⁻¹) * d₁⁻¹ : α) = n₁ * d₁⁻¹ + n₂ * d₂⁻¹,
id                                    └┘   └┘     └┘   └┘
src  ───┘           └┘     └─┘ └┘           
typ  ───┘           └┘     └─┘└┘└┘ └┘   └┘ └┘
doc  ───┘           └┘     └─┘ └┘            
txt  ───┘           └┘     └─┘ └┘            
par  ───┘           └┘     └─┘ └┘            
pid  ───┘           └┘     └─┘ └┘            
st   ───────────────────────────────────────────────────────┘└─
 88    { rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero],
id           └────────────────┘  └────────────────┘  └────────────────┘
src      └──┘└────────────────┘└┘└────────────────┘└┘└────────────────┘
typ      └──┘└────────────────┘└┘└────────────────┘└┘└────────────────┘
doc      └──┘                  └┘                  └┘                  
txt      └──┘                  └┘                  └┘                  
par      └──┘                  └┘                  └┘                  
pid        └┘                  └┘                  └┘                  
st   ───┘└────────────────────┘└──────────────────┘└──────────────────┘└──
 89      { simpa [division_def, left_distrib, right_distrib, mul_inv_eq,
id                └──────────┘  └──────────┘  └───────────┘  └────────┘
src        └─────┘└──────────┘└┘└──────────┘└┘└───────────┘└┘└────────┘└─
typ        └─────┘└──────────┘└┘└──────────┘└┘└───────────┘└┘└────────┘└─
doc        └─────┘            └┘            └┘             └┘          └─
txt        └─────┘            └┘            └┘             └┘          └─
par        └─────┘            └┘            └┘             └┘          └─
pid                         └┘            └┘             └┘          └─
st   ─────┘└─────────────────────────────────────────────────────────────
 90               d₁0, d₂0, division_ring.mul_ne_zero d₁0 d₂0, mul_assoc] },
id                └─┘  └─┘  └───────────────────────┘ └─┘ └─┘  └───────┘
src  ────────────┘   └┘   └┘└───────────────────────┘      └┘└───────┘└┘
typ  ────────────┘└─┘└┘└─┘└┘└───────────────────────┘└─┘└─┘└┘└───────┘└┘
doc  ────────────┘   └┘   └┘                               └┘         └┘
txt  ────────────┘   └┘   └┘                               └┘         └┘
par  ────────────┘   └┘   └┘                               └┘         └┘
pid  ────────────┘   └┘   └┘                               └┘         
st   ────────────────────────────────────────────────────────────────────┘└┘
 91      all_goals {simp [d₁0, d₂0, division_ring.mul_ne_zero d₁0 d₂0]} },
id                        └─┘  └─┘  └───────────────────────┘ └─┘ └─┘
src      └─────────┘└────┘   └┘   └┘└───────────────────────┘      └┘
typ      └─────────┘└────┘└─┘└┘└─┘└┘└───────────────────────┘└─┘└─┘└┘
doc      └─────────┘└────┘   └┘   └┘                               └┘
txt      └─────────┘└────┘   └┘   └┘                               └┘
par      └─────────┘└────┘   └┘   └┘                               └┘
pid               └──────┘   └┘   └┘                               └┘
st   ──────────────┘└────────────────────────────────────────────────┘└┘
 92    rw [← mul_assoc (d₂:α), mul_inv_cancel d₂0, one_mul,
id           └───────┘  └┘    └────────────┘ └─┘  └─────┘
src    └────┘└───────┘    └─┘└────────────┘   └┘└─────┘└─
typ    └────┘└───────┘ └┘└─┘└────────────┘└─┘└┘└─────┘└─
doc    └────┘             └─┘                 └┘       └─
txt    └────┘             └─┘                 └┘       └─
par    └────┘             └─┘                 └┘       └─
pid      └──┘             └─┘                 └┘       └─
st   ───────────────────────┘└──────────────────┘└───────┘└─
 93        ← nat.mul_cast_comm], simp [d₁0, mul_assoc]
id           └───────────────┘         └─┘  └───────┘
src  ───────┘└───────────────┘  └────┘   └┘└───────┘└┘
typ  ───────┘└───────────────┘  └────┘└─┘└┘└───────┘└┘
doc  ───────┘                   └────┘   └┘         └┘
txt  ───────┘                   └────┘   └┘         └┘
par  ───────┘                   └────┘   └┘         └┘
pid  ───────┘                          └┘         
st   ────────────────────────┘└───────────────────────┘
 94  end
st   └─┘
 95  
 96  @[simp, move_cast] theorem cast_neg : ∀ n, ((-n : ℚ) : α) = -n
id                                                         
src                                                           
typ                                                        
doc    └──┘  └───────┘                                 
 97  | ⟨n, d, h, c⟩ := show (↑-n * d⁻¹ : α) = -(n * d⁻¹),
id                             └┘           └┘
src                              └┘            └┘
typ                            └┘           └┘
 98    by rw [int.cast_neg, neg_mul_eq_neg_mul]
id            └──────────┘  └────────────────┘
src       └──┘└──────────┘└┘└────────────────┘└─
typ       └──┘└──────────┘└┘└────────────────┘└─
doc       └──┘            └┘                  └─
txt       └──┘            └┘                  └─
par       └──┘            └┘                  └─
pid         └┘            └┘                  
st       └───────────────┘└──────────────────┘
 99  
src  
typ  
doc  
txt  
par  
pid  
st   
100  @[move_cast] theorem cast_sub_of_ne_zero {m n : ℚ}
id                                                   
src                                                  
typ                                                  
doc    └───────┘                                     
101    (m0 : (m.denom : α) ≠ 0) (n0 : (n.denom : α) ≠ 0) : ((m - n : ℚ) : α) = m - n :=
id            └────┘                └────┘                           
src            └────┘                  └────┘                               
typ           └────┘                └────┘                           
doc                                                                  
102  have ((-n).denom : α) ≠ 0, by cases n; exact n0,
id           └───┘                           └┘
src           └───┘              └────┘   └────┘
typ          └───┘             └────┘  └────┘└┘
doc                                └────┘   └────┘
txt                                └────┘   └────┘
par                                └────┘   └────┘
pid                                             
st                                └────────────────┘
103  by simp [(cast_add_of_ne_zero m0 this)]
id             └─────────────────┘ └┘ └──┘
src     └────┘ └─────────────────┘      └──
typ     └────┘ └─────────────────┘└┘└──┘└──
doc     └────┘                          └──
txt     └────┘                          └──
par     └────┘                          └──
pid                                   └┘
st     └─────────────────────────────────────
104  
src  
typ  
doc  
txt  
par  
pid  
st   
105  @[move_cast] theorem cast_mul_of_ne_zero : ∀ {m n : ℚ},
id                                                      
src                                                      
typ                                                     
doc    └───────┘                                         
106    (m.denom : α) ≠ 0 → (n.denom : α) ≠ 0 → ((m * n : ℚ) : α) = m * n
id      └────┘           └────┘                          
src      └────┘             └────┘                              
typ     └────┘           └────┘                          
doc                                                      
107  | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := λ (d₁0 : (d₁:α) ≠ 0) (d₂0 : (d₂:α) ≠ 0), begin
id          └┘               └┘                                             
src                                                                           
typ         └┘               └┘                                             
st                                                                                   └─────
108    have d₁0' : (d₁:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d₁0; exact d₁0 rfl),
id                  └┘         └─────────────────┘                              └─┘ └─┘
src    └──────────┘   └┘└────┘└─────────────────┘└─┘  └──┘  └─┘ └─────┘└┘└────┘   └─┘
typ    └──────────┘ └┘└┘└────┘└─────────────────┘└─┘  └──┘  └─┘└─────┘└┘└────┘└─┘└─┘
doc    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
txt    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
par    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
pid    └───────┘└─┘    └┘ └───┘                   └─┘  └──┘  └──┘ └─────────────┘      
st   ─────────────────────────────────────────────────────────┘└─────────────────────────┘└─
109    have d₂0' : (d₂:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d₂0; exact d₂0 rfl),
id                  └┘           └─────────────────┘                              └─┘ └─┘
src    └──────────┘    └┘ └────┘└─────────────────┘└─┘  └──┘  └─┘ └─────┘└┘└────┘   └─┘
typ    └──────────┘ └┘ └┘ └────┘└─────────────────┘└─┘  └──┘  └─┘└─────┘└┘└────┘└─┘└─┘
doc    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
txt    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
par    └──────────┘    └┘ └────┘                   └─┘  └──┘  └─┘ └─────┘└┘└────┘      
pid    └───────┘└─┘    └┘ └───┘                   └─┘  └──┘  └──┘ └─────────────┘      
st   ─────────────────────────────────────────────────────────┘└─────────────────────────┘└─
110    rw [num_denom', num_denom', mul_def d₁0' d₂0'],
id         └────────┘  └────────┘  └─────┘ └──┘ └──┘
src    └──┘└────────┘└┘└────────┘└┘└─────┘        
typ    └──┘└────────┘└┘└────────┘└┘└─────┘└──┘└──┘
doc    └──┘          └┘          └┘               
txt    └──┘          └┘          └┘               
par    └──┘          └┘          └┘               
pid      └┘          └┘          └┘               
st   ───────────────┘└──────────┘└─────────────────┘└──
111    suffices : (n₁ * ((n₂ * d₂⁻¹) * d₁⁻¹) : α) = n₁ * (d₁⁻¹ * (n₂ * d₂⁻¹)),
id                              └┘               └┘    └┘      └┘   └┘
src    └─────────┘          └┘└┘     └──┘ └┘                 └┘
typ    └─────────┘          └┘└┘     └──┘└┘└┘  └┘    └┘ └┘  └┘
doc    └─────────┘             └┘     └──┘ └┘                  └┘
txt    └─────────┘             └┘     └──┘ └┘                  └┘
par    └─────────┘             └┘     └──┘ └┘                  └┘
pid    └───────┘└┘             └┘     └──┘ └┘                  └┘
st   ───────────────────────────────────────────────────────────────────────┘└─
112    { rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero],
id           └────────────────┘  └────────────────┘  └────────────────┘
src      └──┘└────────────────┘└┘└────────────────┘└┘└────────────────┘
typ      └──┘└────────────────┘└┘└────────────────┘└┘└────────────────┘
doc      └──┘                  └┘                  └┘                  
txt      └──┘                  └┘                  └┘                  
par      └──┘                  └┘                  └┘                  
pid        └┘                  └┘                  └┘                  
st   ───┘└────────────────────┘└──────────────────┘└──────────────────┘└──
113      { simpa [division_def, mul_inv_eq, d₁0, d₂0, division_ring.mul_ne_zero d₁0 d₂0, mul_assoc] },
id                └──────────┘  └────────┘  └─┘  └─┘  └───────────────────────┘ └─┘ └─┘  └───────┘
src        └─────┘└──────────┘└┘└────────┘└┘   └┘   └┘└───────────────────────┘      └┘└───────┘└┘
typ        └─────┘└──────────┘└┘└────────┘└┘└─┘└┘└─┘└┘└───────────────────────┘└─┘└─┘└┘└───────┘└┘
doc        └─────┘            └┘          └┘   └┘   └┘                               └┘         └┘
txt        └─────┘            └┘          └┘   └┘   └┘                               └┘         └┘
par        └─────┘            └┘          └┘   └┘   └┘                               └┘         └┘
pid                         └┘          └┘   └┘   └┘                               └┘         
st   ─────┘└───────────────────────────────────────────────────────────────────────────────────────┘└┘
114      all_goals {simp [d₁0, d₂0, division_ring.mul_ne_zero d₁0 d₂0]} },
id                        └─┘  └─┘  └───────────────────────┘ └─┘ └─┘
src      └─────────┘└────┘   └┘   └┘└───────────────────────┘      └┘
typ      └─────────┘└────┘└─┘└┘└─┘└┘└───────────────────────┘└─┘└─┘└┘
doc      └─────────┘└────┘   └┘   └┘                               └┘
txt      └─────────┘└────┘   └┘   └┘                               └┘
par      └─────────┘└────┘   └┘   └┘                               └┘
pid               └──────┘   └┘   └┘                               └┘
st   ──────────────┘└────────────────────────────────────────────────┘└┘
115    rw [division_ring.inv_comm_of_comm d₁0 (nat.mul_cast_comm _ _).symm]
id         └────────────────────────────┘ └─┘  └───────────────┘
src    └──┘└────────────────────────────┘    └───────────────┘└──────────┘
typ    └──┘└────────────────────────────┘└─┘ └───────────────┘└──────────┘
doc    └──┘                                                   └──────────┘
txt    └──┘                                                   └──────────┘
par    └──┘                                                   └──────────┘
pid      └┘                                                   └─────────┘
st   ───────────────────────────────────────────────────────────────────┘└┘
116  end
st   └─┘
117  
118  @[move_cast] theorem cast_inv_of_ne_zero : ∀ {n : ℚ},
id                                                    
src                                                    
typ                                                   
doc    └───────┘                                       
119    (n.num : α) ≠ 0 → (n.denom : α) ≠ 0 → ((n⁻¹ : ℚ) : α) = n⁻¹
id      └──┘           └────┘            └┘          └┘
src      └──┘             └────┘              └┘            └┘
typ     └──┘           └────┘            └┘          └┘
doc                                                  
120  | ⟨n, d, h, c⟩ := λ (n0 : (n:α) ≠ 0) (d0 : (d:α) ≠ 0), begin
id                                               
src                                                  
typ                                              
st                                                          └─────
121    have n0' : (n:ℤ) ≠ 0 := λ e, by rw e at n0; exact n0 rfl,
id                                                    └┘ └─┘
src    └─────────┘   └┘└────┘ └──┘  └─┘ └────┘└┘└────┘  └─┘
typ    └─────────┘  └┘└────┘ └──┘  └─┘└────┘└┘└────┘└┘└─┘
doc    └─────────┘   └┘ └────┘ └──┘  └─┘ └────┘└┘└────┘  
txt    └─────────┘   └┘ └────┘ └──┘  └─┘ └────┘└┘└────┘  
par    └─────────┘   └┘ └────┘ └──┘  └─┘ └────┘└┘└────┘  
pid    └──────┘└─┘   └┘ └───┘ └──┘  └──┘ └────────────┘  
st   ────────────────────────────────┘└───────────────────────┘└─
122    have d0' : (d:ℤ) ≠ 0 := int.coe_nat_ne_zero.2 (λ e, by rw e at d0; exact d0 rfl),
id                            └─────────────────┘                             └┘ └─┘
src    └─────────┘   └┘ └────┘└─────────────────┘└─┘  └──┘  └─┘ └────┘└┘└────┘  └─┘
typ    └─────────┘  └┘ └────┘└─────────────────┘└─┘  └──┘  └─┘└────┘└┘└────┘└┘└─┘
doc    └─────────┘   └┘ └────┘                   └─┘  └──┘  └─┘ └────┘└┘└────┘     
txt    └─────────┘   └┘ └────┘                   └─┘  └──┘  └─┘ └────┘└┘└────┘     
par    └─────────┘   └┘ └────┘                   └─┘  └──┘  └─┘ └────┘└┘└────┘     
pid    └──────┘└─┘   └┘ └───┘                   └─┘  └──┘  └──┘ └────────────┘     
st   ───────────────────────────────────────────────────────┘└───────────────────────┘└─
123    rw [num_denom', inv_def],
id         └────────┘  └─────┘
src    └──┘└────────┘└┘└─────┘
typ    └──┘└────────┘└┘└─────┘
doc    └──┘          └┘       
txt    └──┘          └┘       
par    └──┘          └┘       
pid      └┘          └┘       
st   ───────────────┘└───────┘└──
124    rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, inv_div];
id         └────────────────┘  └────────────────┘  └─────┘
src    └──┘└────────────────┘└┘└────────────────┘└┘└─────┘
typ    └──┘└────────────────┘└┘└────────────────┘└┘└─────┘
doc    └──┘                  └┘                  └┘       
txt    └──┘                  └┘                  └┘       
par    └──┘                  └┘                  └┘       
pid      └┘                  └┘                  └┘       
st   ───────────────────────┘└──────────────────┘└───────┘└─
125    simp [n0, d0]
id           └┘  └┘
src    └────┘  └┘  └┘
typ    └────┘└┘└┘└┘└┘
doc    └────┘  └┘  └┘
txt    └────┘  └┘  └┘
par    └────┘  └┘  └┘
pid          └┘  
st   ───────────────┘
126  end
st   └─┘
127  
128  @[move_cast] theorem cast_div_of_ne_zero {m n : ℚ} (md : (m.denom : α) ≠ 0)
id                                                            └────┘     
src                                                            └────┘      
typ                                                           └────┘     
doc    └───────┘                                     
129    (nn : (n.num : α) ≠ 0) (nd : (n.denom : α) ≠ 0) : ((m / n : ℚ) : α) = m / n :=
id            └──┘                └────┘                           
src            └──┘                  └────┘                               
typ           └──┘                └────┘                           
doc                                                                
130  have (n⁻¹.denom : ℤ) ∣ n.num,
id         └┘└───┘       └──┘
src         └┘└───┘        └──┘
typ        └┘└───┘       └──┘
131  by conv in n⁻¹.denom { rw [←(@num_denom n), inv_def] };
id              └┘                └───────┘    └─────┘
src     └──────┘ └┘└───────┘└───┘  └───────┘ └─┘└─────┘└┘
typ     └──────┘└┘└───────┘└───┘  └───────┘└─┘└─────┘└┘
txt     └──────┘   └───────┘└───┘            └─┘       └┘
par     └──────┘   └───────┘└───┘            └─┘       └┘
pid         └─┘   └───┘└───────┘            └─┘       └─┘
st     └──────────────────┘└──────────────────┘└───────┘ └┘
132     apply denom_dvd,
id            └───────┘
src     └────┘└───────┘
typ     └────┘└───────┘
doc     └────┘
txt     └────┘
par     └────┘
pid          
st   ─────────────────┘
133  have (n⁻¹.denom : α) = 0 → (n.num : α) = 0, from
id         └┘└───┘            └──┘     
src         └┘└───┘              └──┘      
typ        └┘└───┘            └──┘     
134  λ h, let ⟨k, e⟩ := this in
id       └─┘           └──┘
typ      └─┘           └──┘
135    by have := congr_arg (coe : ℤ → α) e;
id                └───────┘  └─┘         
src       └──────┘└───────┘ └─┘└─┘   └┘
typ       └──────┘└───────┘ └─┘└─┘  └┘
doc       └──────┘             └─┘   └┘
txt       └──────┘             └─┘   └┘
par       └──────┘             └─┘   └┘
pid       └───┘└─┘             └─┘   └┘
st       └───────────────────────────────────
136       rwa [int.cast_mul, int.cast_coe_nat, h, zero_mul] at this,
id             └──────────┘  └──────────────┘    └──────┘
src       └───┘└──────────┘└┘└──────────────┘└┘ └┘└──────┘└───────┘
typ       └───┘└──────────┘└┘└──────────────┘└┘└┘└──────┘└───────┘
doc       └───┘            └┘                └┘ └┘        └───────┘
txt       └───┘            └┘                └┘ └┘        └───────┘
par       └───┘            └┘                └┘ └┘        └───────┘
pid          └┘            └┘                └┘ └┘        └──────┘
st   ─────────┘└──────────┘└────────────────┘└─┘└────────┘└──────┘
137  by rw [division_def, cast_mul_of_ne_zero md (mt this nn), cast_inv_of_ne_zero nn nd, division_def]
id          └──────────┘  └─────────────────┘ └┘  └┘ └──┘ └┘   └─────────────────┘ └┘ └┘  └──────────┘
src     └──┘└──────────┘└┘└─────────────────┘   └┘      └─┘└─────────────────┘    └┘└──────────┘└─
typ     └──┘└──────────┘└┘└─────────────────┘└┘ └┘└──┘└┘└─┘└─────────────────┘└┘└┘└┘└──────────┘└─
doc     └──┘            └┘                              └─┘                       └┘            └─
txt     └──┘            └┘                              └─┘                       └┘            └─
par     └──┘            └┘                              └─┘                       └┘            └─
pid       └┘            └┘                              └─┘                       └┘            
st     └───────────────┘└───────────────────────────────────┘└─────────────────────────┘└────────────┘
138  
src  
typ  
doc  
txt  
par  
pid  
st   
139  @[simp, elim_cast] theorem cast_inj [char_zero α] : ∀ {m n : ℚ}, (m : α) = n ↔ m = n
id                                        └───────┘                           
src                                       └───────┘                                
typ                                       └───────┘                           
doc    └──┘  └───────┘                    └───────┘               
140  | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := begin
st                                          └─────
141    refine ⟨λ h, _, congr_arg _⟩,
id                     └───────┘
src    └─────┘  └─────┘└───────┘└─┘
typ    └─────┘  └─────┘└───────┘└─┘
doc    └─────┘  └─────┘         └─┘
txt    └─────┘  └─────┘         └─┘
par    └─────┘  └─────┘         └─┘
pid            └─────┘         └─┘
st   ─────────────────────────────┘└─
142    have d₁0 : d₁ ≠ 0 := ne_of_gt h₁,
id                └┘       └──────┘ └┘
src    └─────────┘  └────┘└──────┘
typ    └─────────┘└┘└────┘└──────┘└┘
doc    └─────────┘   └────┘        
txt    └─────────┘   └────┘        
par    └─────────┘   └────┘        
pid    └──────┘└─┘   └───┘        
st   ─────────────────────────────────┘└─
143    have d₂0 : d₂ ≠ 0 := ne_of_gt h₂,
id                └┘        └──────┘ └┘
src    └─────────┘   └────┘└──────┘
typ    └─────────┘└┘ └────┘└──────┘└┘
doc    └─────────┘   └────┘        
txt    └─────────┘   └────┘        
par    └─────────┘   └────┘        
pid    └──────┘└─┘   └───┘        
st   ─────────────────────────────────┘└─
144    have d₁a : (d₁:α) ≠ 0 := nat.cast_ne_zero.2 d₁0,
id                 └┘          └──────────────┘   └─┘
src    └─────────┘    └┘ └────┘└──────────────┘└─┘
typ    └─────────┘ └┘└┘ └────┘└──────────────┘└─┘└─┘
doc    └─────────┘    └┘ └────┘                └─┘
txt    └─────────┘    └┘ └────┘                └─┘
par    └─────────┘    └┘ └────┘                └─┘
pid    └──────┘└─┘    └┘ └───┘                └─┘
st   ────────────────────────────────────────────────┘└─
145    have d₂a : (d₂:α) ≠ 0 := nat.cast_ne_zero.2 d₂0,
id                 └┘          └──────────────┘   └─┘
src    └─────────┘    └┘ └────┘└──────────────┘└─┘
typ    └─────────┘ └┘└┘ └────┘└──────────────┘└─┘└─┘
doc    └─────────┘    └┘ └────┘                └─┘
txt    └─────────┘    └┘ └────┘                └─┘
par    └─────────┘    └┘ └────┘                └─┘
pid    └──────┘└─┘    └┘ └───┘                └─┘
st   ────────────────────────────────────────────────┘└─
146    rw [num_denom', num_denom'] at h ⊢,
id         └────────┘  └────────┘
src    └──┘└────────┘└┘└────────┘└──────┘
typ    └──┘└────────┘└┘└────────┘└──────┘
doc    └──┘          └┘          └──────┘
txt    └──┘          └┘          └──────┘
par    └──┘          └┘          └──────┘
pid      └┘          └┘          └─────┘
st   ───────────────┘└──────────┘└─────┘└─
147    rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero] at h; simp [d₁0, d₂0] at h ⊢,
id         └────────────────┘  └────────────────┘              └─┘  └─┘
src    └──┘└────────────────┘└┘└────────────────┘└────┘  └────┘   └┘   └──────┘
typ    └──┘└────────────────┘└┘└────────────────┘└────┘  └────┘└─┘└┘└─┘└──────┘
doc    └──┘                  └┘                  └────┘  └────┘   └┘   └──────┘
txt    └──┘                  └┘                  └────┘  └────┘   └┘   └──────┘
par    └──┘                  └┘                  └────┘  └────┘   └┘   └──────┘
pid      └┘                  └┘                  └───┘         └┘   └────┘
st   ───────────────────────┘└──────────────────┘└───────────────────────────┘└─
148    rwa [eq_div_iff_mul_eq _ _ d₂a, division_def, mul_assoc,
id          └───────────────┘     └─┘  └──────────┘  └───────┘
src    └───┘└───────────────┘└───┘   └┘└──────────┘└┘└───────┘└─
typ    └───┘└───────────────┘└───┘└─┘└┘└──────────┘└┘└───────┘└─
doc    └───┘                 └───┘   └┘            └┘         └─
txt    └───┘                 └───┘   └┘            └┘         └─
par    └───┘                 └───┘   └┘            └┘         └─
pid       └┘                 └───┘   └┘            └┘         └─
st   ───────────────────────────────┘└────────────┘└─────────┘└─
149      division_ring.inv_comm_of_comm d₁a (nat.mul_cast_comm _ _),
id       └────────────────────────────┘ └─┘  └───────────────┘
src  ───┘└────────────────────────────┘    └───────────────┘└──────
typ  ───┘└────────────────────────────┘└─┘ └───────────────┘└──────
doc  ───┘                                                   └──────
txt  ───┘                                                   └──────
par  ───┘                                                   └──────
pid  ───┘                                                   └──────
st   ─────────────────────────────────────────────────────────────┘└─
150      ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq _ _ d₁a, eq_comm,
id         └───────┘    └──────────┘  └─────┘  └───────────────┘     └─┘  └─────┘
src  ─────┘└───────┘└──┘└──────────┘└┘└─────┘└┘└───────────────┘└───┘   └┘└─────┘└─
typ  ─────┘└───────┘└──┘└──────────┘└┘└─────┘└┘└───────────────┘└───┘└─┘└┘└─────┘└─
doc  ─────┘         └──┘            └┘       └┘                 └───┘   └┘       └─
txt  ─────┘         └──┘            └┘       └┘                 └───┘   └┘       └─
par  ─────┘         └──┘            └┘       └┘                 └───┘   └┘       └─
pid  ─────┘         └──┘            └┘       └┘                 └───┘   └┘       └─
st   ──────────────┘└──────────────┘└───────┘└─────────────────────────┘└───────┘└─
151      ← int.cast_coe_nat, ← int.cast_mul, ← int.cast_coe_nat, ← int.cast_mul,
id         └──────────────┘    └──────────┘    └──────────────┘    └──────────┘
src  ─────┘└──────────────┘└──┘└──────────┘└──┘└──────────────┘└──┘└──────────┘└─
typ  ─────┘└──────────────┘└──┘└──────────┘└──┘└──────────────┘└──┘└──────────┘└─
doc  ─────┘                └──┘            └──┘                └──┘            └─
txt  ─────┘                └──┘            └──┘                └──┘            └─
par  ─────┘                └──┘            └──┘                └──┘            └─
pid  ─────┘                └──┘            └──┘                └──┘            └─
st   ─────────────────────┘└──────────────┘└──────────────────┘└──────────────┘└─
152      int.cast_inj, ← mk_eq (int.coe_nat_ne_zero.2 d₁0) (int.coe_nat_ne_zero.2 d₂0)] at h
id       └──────────┘    └───┘                        └─┘   └─────────────────┘   └─┘
src  ───┘└──────────┘└──┘└───┘                    └─┘   └┘ └─────────────────┘└─┘   └──────┘
typ  ───┘└──────────┘└──┘└───┘                    └─┘└─┘└┘ └─────────────────┘└─┘└─┘└──────┘
doc  ───┘            └──┘                         └─┘   └┘                    └─┘   └──────┘
txt  ───┘            └──┘                         └─┘   └┘                    └─┘   └──────┘
par  ───┘            └──┘                         └─┘   └┘                    └─┘   └──────┘
pid  ───┘            └──┘                         └─┘   └┘                    └─┘   └┘└───┘
st   ───────────────┘└───────────────────────────────────────────────────────────────┘└────┘
153  end
st   └─┘
154  
155  theorem cast_injective [char_zero α] : function.injective (coe : ℚ → α)
id                           └───────┘     └────────────────┘  └─┘      
src                          └───────┘      └────────────────┘  └─┘   
typ                          └───────┘     └────────────────┘  └─┘      
doc                          └───────┘                                
156  | m n := cast_inj.1
id            └──────┘
src           └──────┘
typ           └──────┘
157  
158  @[simp] theorem cast_eq_zero [char_zero α] {n : ℚ} : (n : α) = 0 ↔ n = 0 :=
id                                 └───────┘                       
src                                └───────┘                           
typ                                └───────┘                       
doc    └──┘                        └───────┘         
159  by rw [← cast_zero, cast_inj]
id            └───────┘  └──────┘
src     └────┘└───────┘└┘└──────┘└─
typ     └────┘└───────┘└┘└──────┘└─
doc     └────┘         └┘        └─
txt     └────┘         └┘        └─
par     └────┘         └┘        └─
pid       └──┘         └┘        
st     └──────────────┘└────────┘
160  
src  
typ  
doc  
txt  
par  
pid  
st   
161  @[simp] theorem cast_ne_zero [char_zero α] {n : ℚ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
id                                 └───────┘                       
src                                └───────┘                           
typ                                └───────┘                       
doc    └──┘                        └───────┘         
162  not_congr cast_eq_zero
id   └───────┘ └──────────┘
src  └───────┘ └──────────┘
typ  └───────┘ └──────────┘
163  
164  theorem eq_cast_of_ne_zero (f : ℚ → α) (H1 : f 1 = 1)
id                                                 
src                                                  
typ                                                
doc                                  
165    (Hadd : ∀ x y, f (x + y) = f x + f y)
id                             
src                                 
typ                            
166    (Hmul : ∀ x y, f (x * y) = f x * f y) :
id                             
src                                 
typ                            
167    ∀ n : ℚ, (n.denom : α) ≠ 0 → f n = n
id             └────┘             
src              └────┘               
typ            └────┘             
doc          
168  | ⟨n, d, h, c⟩ := λ (h₂ : ((d:ℤ):α) ≠ 0), show _ = (n / (d:ℤ) : α), begin
id                                                           
src                                                         
typ                                                          
st                                                                       └─────
169    rw [num_denom', mk_eq_div, eq_div_iff_mul_eq _ _ h₂],
id         └────────┘  └───────┘  └───────────────┘     └┘
src    └──┘└────────┘└┘└───────┘└┘└───────────────┘└───┘  
typ    └──┘└────────┘└┘└───────┘└┘└───────────────┘└───┘└┘
doc    └──┘          └┘         └┘                 └───┘  
txt    └──┘          └┘         └┘                 └───┘  
par    └──┘          └┘         └┘                 └───┘  
pid      └┘          └┘         └┘                 └───┘  
st   ───────────────┘└─────────┘└────────────────────────┘└──
170    have : ∀ n : ℤ, f n = n, { apply int.eq_cast; simp [H1, Hadd] },
id                                    └─────────┘        └┘  └──┘
src    └─────┘ └───┘         └────┘└─────────┘  └────┘  └┘    └┘
typ    └─────┘ └───┘        └────┘└─────────┘  └────┘└┘└┘└──┘└┘
doc    └─────┘ └───┘          └────┘             └────┘  └┘    └┘
txt    └─────┘ └───┘          └────┘             └────┘  └┘    └┘
par    └─────┘ └───┘          └────┘             └────┘  └┘    └┘
pid    └───┘└┘ └───┘                                  └┘    
st   ────────────────────────┘└──┘└─────────────────────────────────┘└┘
171    rw [← this, ← this, ← Hmul, div_mul_cancel],
id           └──┘    └──┘    └──┘  └────────────┘
src    └────┘    └──┘    └──┘    └┘└────────────┘
typ    └────┘└──┘└──┘└──┘└──┘└──┘└┘└────────────┘
doc    └────┘    └──┘    └──┘    └┘              
txt    └────┘    └──┘    └──┘    └┘              
par    └────┘    └──┘    └──┘    └┘              
pid      └──┘    └──┘    └──┘    └┘              
st   ───────────┘└──────┘└──────┘└──────────────┘└──
172    exact int.cast_ne_zero.2 (int.coe_nat_ne_zero.2 $ ne_of_gt h),
id           └──────────────┘    └─────────────────┘     └──────┘ 
src    └────┘└──────────────┘└─┘ └─────────────────┘└─┘ └──────┘ 
typ    └────┘└──────────────┘└─┘ └─────────────────┘└─┘ └──────┘
doc    └────┘                └─┘                    └─┘          
txt    └────┘                └─┘                    └─┘          
par    └────┘                └─┘                    └─┘          
pid                         └─┘                    └─┘          
st   ──────────────────────────────────────────────────────────────┘└─
173  end
st   ──┘
174  
175  theorem eq_cast [char_zero α] (f : ℚ → α) (H1 : f 1 = 1)
id                    └───────┘                      
src                   └───────┘                         
typ                   └───────┘                      
doc                   └───────┘         
176    (Hadd : ∀ x y, f (x + y) = f x + f y)
id                             
src                                 
typ                            
177    (Hmul : ∀ x y, f (x * y) = f x * f y) (n : ℚ) : f n = n :=
id                                           
src                                                    
typ                                          
doc                                               
178  eq_cast_of_ne_zero _ H1 Hadd Hmul _ $
id   └────────────────┘   └┘ └──┘ └──┘
src  └────────────────┘
typ  └────────────────┘   └┘ └──┘ └──┘
179    nat.cast_ne_zero.2 $ ne_of_gt n.pos
id     └──────────────┘    └──────┘ └──┘
src    └──────────────┘    └──────┘  └──┘
typ    └──────────────┘    └──────┘ └──┘
180  
181  @[simp, move_cast] theorem cast_add [char_zero α] (m n) :
id                                        └───────┘ 
src                                       └───────┘
typ                                       └───────┘ 
doc    └──┘  └───────┘                    └───────┘
182    ((m + n : ℚ) : α) = m + n :=
id                     
src                       
typ                    
doc              
183  cast_add_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
id   └─────────────────┘  └──────────────┘    └──────┘ └──┘   └──────────────┘    └──────┘ └──┘
src  └─────────────────┘  └──────────────┘    └──────┘  └──┘   └──────────────┘    └──────┘  └──┘
typ  └─────────────────┘  └──────────────┘    └──────┘ └──┘   └──────────────┘    └──────┘ └──┘
184  
185  @[simp, move_cast] theorem cast_sub [char_zero α] (m n) :
id                                        └───────┘ 
src                                       └───────┘
typ                                       └───────┘ 
doc    └──┘  └───────┘                    └───────┘
186    ((m - n : ℚ) : α) = m - n :=
id                     
src                       
typ                    
doc              
187  cast_sub_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
id   └─────────────────┘  └──────────────┘    └──────┘ └──┘   └──────────────┘    └──────┘ └──┘
src  └─────────────────┘  └──────────────┘    └──────┘  └──┘   └──────────────┘    └──────┘  └──┘
typ  └─────────────────┘  └──────────────┘    └──────┘ └──┘   └──────────────┘    └──────┘ └──┘
188  
189  @[simp, move_cast] theorem cast_mul [char_zero α] (m n) :
id                                        └───────┘ 
src                                       └───────┘
typ                                       └───────┘ 
doc    └──┘  └───────┘                    └───────┘
190    ((m * n : ℚ) : α) = m * n :=
id                     
src                       
typ                    
doc              
191  cast_mul_of_ne_zero (nat.cast_ne_zero.2 $ ne_of_gt m.pos) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
id   └─────────────────┘  └──────────────┘    └──────┘ └──┘   └──────────────┘    └──────┘ └──┘
src  └─────────────────┘  └──────────────┘    └──────┘  └──┘   └──────────────┘    └──────┘  └──┘
typ  └─────────────────┘  └──────────────┘    └──────┘ └──┘   └──────────────┘    └──────┘ └──┘
192  
193  @[simp, squash_cast, move_cast] theorem cast_bit0 [char_zero α] (n : ℚ) :
id                                                      └───────┘        
src                                                     └───────┘         
typ                                                     └───────┘        
doc    └──┘  └─────────┘  └───────┘                     └───────┘         
194    ((bit0 n : ℚ) : α) = bit0 n :=
id       └──┘           └──┘ 
src      └──┘             └──┘
typ      └──┘           └──┘ 
doc               
195  cast_add _ _
id   └──────┘
src  └──────┘
typ  └──────┘
196  
197  @[simp, squash_cast, move_cast] theorem cast_bit1 [char_zero α] (n : ℚ) :
id                                                      └───────┘        
src                                                     └───────┘         
typ                                                     └───────┘        
doc    └──┘  └─────────┘  └───────┘                     └───────┘         
198    ((bit1 n : ℚ) : α) = bit1 n :=
id       └──┘           └──┘ 
src      └──┘             └──┘
typ      └──┘           └──┘ 
doc               
199  by rw [bit1, cast_add, cast_one, cast_bit0]; refl
id          └──┘  └──────┘  └──────┘  └───────┘
src     └──┘└──┘└┘└──────┘└┘└──────┘└┘└───────┘  └────
typ     └──┘└──┘└┘└──────┘└┘└──────┘└┘└───────┘  └────
doc     └──┘    └┘        └┘        └┘           └────
txt     └──┘    └┘        └┘        └┘           └────
par     └──┘    └┘        └┘        └┘           └────
pid       └┘    └┘        └┘        └┘               
st     └───────┘└────────┘└────────┘└─────────┘└──────
200  
src  
typ  
doc  
txt  
par  
pid  
st   
201  instance is_ring_hom_cast [char_zero α] : is_ring_hom (rat.cast : ℚ → α) :=
id                              └───────┘     └─────────┘  └──────┘      
src                             └───────┘      └─────────┘  └──────┘   
typ                             └───────┘     └─────────┘  └──────┘      
doc                             └───────┘      └─────────┘  └──────┘   
202  ⟨rat.cast_one, rat.cast_mul, rat.cast_add⟩
id    └──────────┘  └──────────┘  └──────────┘
src   └──────────┘  └──────────┘  └──────────┘
typ   └──────────┘  └──────────┘  └──────────┘
203  
204  end with_div_ring
205  
206  @[move_cast] theorem cast_mk [discrete_field α] [char_zero α] (a b : ℤ) : ((a /. b) : α) = a / b :=
id                                 └────────────┘    └───────┘                 └┘          
src                                └────────────┘     └───────┘                   └┘            
typ                                └────────────┘    └───────┘                 └┘          
doc    └───────┘                                      └───────┘                    └┘
207  if b0 : b = 0 then by simp [b0, div_zero]
id   └┘                        └┘  └──────┘
src  └┘                   └────┘  └┘└──────┘└┘
typ  └┘                  └────┘└┘└┘└──────┘└┘
doc                        └────┘  └┘        └┘
txt                        └────┘  └┘        └┘
par                        └────┘  └┘        └┘
pid                              └┘        
st                        └───────────────────┘
208  else cast_mk_of_ne_zero a b (int.cast_ne_zero.2 b0)
id        └────────────────┘    └──────────────┘  └┘
src       └────────────────┘      └──────────────┘
typ       └────────────────┘    └──────────────┘  └┘
209  
210  @[simp, move_cast] theorem cast_inv [discrete_field α] [char_zero α] (n) : ((n⁻¹ : ℚ) : α) = n⁻¹ :=
id                                        └────────────┘    └───────┘           └┘          └┘
src                                       └────────────┘     └───────┘             └┘            └┘
typ                                       └────────────┘    └───────┘           └┘          └┘
doc    └──┘  └───────┘                                       └───────┘                  
211  if n0 : n.num = 0 then
id   └┘      └──┘ 
src  └┘       └──┘ 
typ  └┘      └──┘ 
212    by simp [show n = 0, by rw [←(@num_denom n), n0]; simp, inv_zero] else
id                                  └───────┘    └┘         └──────┘
src       └────┘     └─────┘└───┘  └───────┘ └─┘  └──────┘└──────┘└┘
typ       └────┘    └─────┘└───┘  └───────┘└─┘└┘└──────┘└──────┘└┘
doc       └────┘      └─────┘└───┘            └─┘  └──────┘        └┘
txt       └────┘      └─────┘└───┘            └─┘  └──────┘        └┘
par       └────┘      └─────┘└───┘            └─┘  └──────┘        └┘
pid                 └──────────┘            └─┘  └───────┘        
st       └───────────────────┘└──────────────────┘└──┘└────┘└──────────┘
213  cast_inv_of_ne_zero (int.cast_ne_zero.2 n0) (nat.cast_ne_zero.2 $ ne_of_gt n.pos)
id   └─────────────────┘  └──────────────┘  └┘   └──────────────┘    └──────┘ └──┘
src  └─────────────────┘  └──────────────┘       └──────────────┘    └──────┘  └──┘
typ  └─────────────────┘  └──────────────┘  └┘   └──────────────┘    └──────┘ └──┘
214  
215  @[simp, move_cast] theorem cast_div [discrete_field α] [char_zero α] (m n) :
id                                        └────────────┘    └───────┘ 
src                                       └────────────┘     └───────┘
typ                                       └────────────┘    └───────┘ 
doc    └──┘  └───────┘                                       └───────┘
216    ((m / n : ℚ) : α) = m / n :=
id                     
src                       
typ                    
doc              
217  by rw [division_def, cast_mul, cast_inv, division_def]
id          └──────────┘  └──────┘  └──────┘  └──────────┘
src     └──┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────┘└─
typ     └──┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────┘└─
doc     └──┘            └┘        └┘        └┘            └─
txt     └──┘            └┘        └┘        └┘            └─
par     └──┘            └┘        └┘        └┘            └─
pid       └┘            └┘        └┘        └┘            
st     └───────────────┘└────────┘└────────┘└────────────┘
218  
src  
typ  
doc  
txt  
par  
pid  
st   
219  @[simp, move_cast] theorem cast_pow [discrete_field α] [char_zero α] (q) (k : ℕ) :
id                                        └────────────┘    └───────┘            
src                                       └────────────┘     └───────┘             
typ                                       └────────────┘    └───────┘            
doc    └──┘  └───────┘                                       └───────┘
220    ((q ^ k : ℚ) : α) = q ^ k :=
id                     
src                       
typ                    
doc              
221  by induction k; simp only [*, cast_one, cast_mul, pow_zero, pow_succ]
id                                └──────┘  └──────┘  └──────┘  └──────┘
src     └────────┘   └────────────┘└──────┘└┘└──────┘└┘└──────┘└┘└──────┘└─
typ     └────────┘  └────────────┘└──────┘└┘└──────┘└┘└──────┘└┘└──────┘└─
doc     └────────┘   └────────────┘        └┘        └┘        └┘        └─
txt     └────────┘   └────────────┘        └┘        └┘        └┘        └─
par     └────────┘   └────────────┘        └┘        └┘        └┘        └─
pid                     └──┘└───┘        └┘        └┘        └┘        
st     └───────────────────────────────────────────────────────────────────
222  
src  
typ  
doc  
txt  
par  
pid  
st   
223  @[simp] theorem cast_nonneg [linear_ordered_field α] : ∀ {n : ℚ}, 0 ≤ (n : α) ↔ 0 ≤ n
id                                └──────────────────┘                           
src                               └──────────────────┘                              
typ                               └──────────────────┘                           
doc    └──┘                                                        
224  | ⟨n, d, h, c⟩ := show 0 ≤ (n * d⁻¹ : α) ↔ 0 ≤ (⟨n, d, h, c⟩ : ℚ),
id                              └┘                         
src                                 └┘                          
typ                             └┘                         
doc                                                                 
225    by rw [num_denom', ← nonneg_iff_zero_le, mk_nonneg _ (int.coe_nat_pos.2 h),
id            └────────┘    └────────────────┘  └───────┘    └─────────────┘   
src       └──┘└────────┘└──┘└────────────────┘└┘└───────┘└─┘ └─────────────┘└─┘ └──
typ       └──┘└────────┘└──┘└────────────────┘└┘└───────┘└─┘ └─────────────┘└─┘└──
doc       └──┘          └──┘                  └┘         └─┘                └─┘ └──
txt       └──┘          └──┘                  └┘         └─┘                └─┘ └──
par       └──┘          └──┘                  └┘         └─┘                └─┘ └──
pid         └┘          └──┘                  └┘         └─┘                └─┘ └──
st       └─────────────┘└────────────────────┘└─────────────────────────────────┘└─
226      mul_nonneg_iff_right_nonneg_of_pos (@inv_pos α _ _ (nat.cast_pos.2 h)),
id       └────────────────────────────────┘   └─────┘       └──────────┘   
src  ───┘└────────────────────────────────┘  └─────┘ └───┘ └──────────┘└─┘ └───
typ  ───┘└────────────────────────────────┘  └─────┘└───┘ └──────────┘└─┘└───
doc  ───┘                                            └───┘             └─┘ └───
txt  ───┘                                            └───┘             └─┘ └───
par  ───┘                                            └───┘             └─┘ └───
pid  ───┘                                            └───┘             └─┘ └───
st   ─────────────────────────────────────────────────────────────────────────┘└─
227      int.cast_nonneg]
id       └─────────────┘
src  ───┘└─────────────┘└─
typ  ───┘└─────────────┘└─
doc  ───┘               └─
txt  ───┘               └─
par  ───┘               └─
pid  ───┘               
st   ──────────────────┘
228  
src  
typ  
doc  
txt  
par  
pid  
st   
229  @[simp, elim_cast] theorem cast_le [linear_ordered_field α] {m n : ℚ} : (m : α) ≤ n ↔ m ≤ n :=
id                                       └──────────────────┘                         
src                                      └──────────────────┘                             
typ                                      └──────────────────┘                         
doc    └──┘  └───────┘                                                  
230  by rw [← sub_nonneg, ← cast_sub, cast_nonneg, sub_nonneg]
id            └────────┘    └──────┘  └─────────┘  └────────┘
src     └────┘└────────┘└──┘└──────┘└┘└─────────┘└┘└────────┘└─
typ     └────┘└────────┘└──┘└──────┘└┘└─────────┘└┘└────────┘└─
doc     └────┘          └──┘        └┘           └┘          └─
txt     └────┘          └──┘        └┘           └┘          └─
par     └────┘          └──┘        └┘           └┘          └─
pid       └──┘          └──┘        └┘           └┘          
st     └───────────────┘└──────────┘└───────────┘└──────────┘
231  
src  
typ  
doc  
txt  
par  
pid  
st   
232  @[simp, elim_cast] theorem cast_lt [linear_ordered_field α] {m n : ℚ} : (m : α) < n ↔ m < n :=
id                                       └──────────────────┘                         
src                                      └──────────────────┘                             
typ                                      └──────────────────┘                         
doc    └──┘  └───────┘                                                  
233  by simpa [-cast_le] using not_congr (@cast_le α _ n m)
id                             └───────┘   └─────┘     
src     └─────────────────────┘└───────┘  └─────┘ └─┘  └─
typ     └─────────────────────┘└───────┘  └─────┘└─┘└─
doc     └─────────────────────┘                   └─┘  └─
txt     └─────────────────────┘                   └─┘  └─
par     └─────────────────────┘                   └─┘  └─
pid          └────────┘└────┘                   └─┘  
st     └────────────────────────────────────────────────────
234  
src  
typ  
doc  
txt  
par  
pid  
st   
235  @[simp] theorem cast_nonpos [linear_ordered_field α] {n : ℚ} : (n : α) ≤ 0 ↔ n ≤ 0 :=
id                                └──────────────────┘                       
src                               └──────────────────┘                           
typ                               └──────────────────┘                       
doc    └──┘                                                    
236  by rw [← cast_zero, cast_le]
id            └───────┘  └─────┘
src     └────┘└───────┘└┘└─────┘└─
typ     └────┘└───────┘└┘└─────┘└─
doc     └────┘         └┘       └─
txt     └────┘         └┘       └─
par     └────┘         └┘       └─
pid       └──┘         └┘       
st     └──────────────┘└───────┘
237  
src  
typ  
doc  
txt  
par  
pid  
st   
238  @[simp] theorem cast_pos [linear_ordered_field α] {n : ℚ} : (0 : α) < n ↔ 0 < n :=
id                             └──────────────────┘                         
src                            └──────────────────┘                           
typ                            └──────────────────┘                         
doc    └──┘                                                 
239  by rw [← cast_zero, cast_lt]
id            └───────┘  └─────┘
src     └────┘└───────┘└┘└─────┘└─
typ     └────┘└───────┘└┘└─────┘└─
doc     └────┘         └┘       └─
txt     └────┘         └┘       └─
par     └────┘         └┘       └─
pid       └──┘         └┘       
st     └──────────────┘└───────┘
240  
src  
typ  
doc  
txt  
par  
pid  
st   
241  @[simp] theorem cast_lt_zero [linear_ordered_field α] {n : ℚ} : (n : α) < 0 ↔ n < 0 :=
id                                 └──────────────────┘                       
src                                └──────────────────┘                           
typ                                └──────────────────┘                       
doc    └──┘                                                     
242  by rw [← cast_zero, cast_lt]
id            └───────┘  └─────┘
src     └────┘└───────┘└┘└─────┘└─
typ     └────┘└───────┘└┘└─────┘└─
doc     └────┘         └┘       └─
txt     └────┘         └┘       └─
par     └────┘         └┘       └─
pid       └──┘         └┘       
st     └──────────────┘└───────┘
243  
src  
typ  
doc  
txt  
par  
pid  
st   
244  @[simp, squash_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
id                                                   
src                                                   
typ                                                  
doc    └──┘  └─────────┘                          
245  | ⟨n, d, h, c⟩ := show (n / (d : ℤ) : ℚ) = _, by rw [num_denom', mk_eq_div]
id                                                  └────────┘  └───────┘
src                                               └──┘└────────┘└┘└───────┘└─
typ                                             └──┘└────────┘└┘└───────┘└─
doc                                                  └──┘          └┘         └─
txt                                                   └──┘          └┘         └─
par                                                   └──┘          └┘         └─
pid                                                     └┘          └┘         
st                                                   └─────────────┘└─────────┘
246  
src  
typ  
doc  
txt  
par  
pid  
st   
247  @[simp, move_cast] theorem cast_min [discrete_linear_ordered_field α] {a b : ℚ} :
id                                        └───────────────────────────┘          
src                                       └───────────────────────────┘           
typ                                       └───────────────────────────┘          
doc    └──┘  └───────┘                                                            
248    (↑(min a b) : α) = min a b :=
id       └─┘         └─┘  
src      └─┘            └─┘
typ      └─┘         └─┘  
249  by by_cases a ≤ b; simp [h, min]
id                           └─┘
src     └───────┘    └────┘ └┘└─┘└─
typ     └───────┘  └────┘└┘└─┘└─
doc     └───────┘     └────┘ └┘   └─
txt     └───────┘     └────┘ └┘   └─
par     └───────┘     └────┘ └┘   └─
pid                       └┘   
st     └──────────────────────────────
250  
src  
typ  
doc  
txt  
par  
pid  
st   
251  @[simp, move_cast] theorem cast_max [discrete_linear_ordered_field α] {a b : ℚ} :
id                                        └───────────────────────────┘          
src                                       └───────────────────────────┘           
typ                                       └───────────────────────────┘          
doc    └──┘  └───────┘                                                            
252    (↑(max a b) : α) = max a b :=
id       └─┘         └─┘  
src      └─┘            └─┘
typ      └─┘         └─┘  
253  by by_cases a ≤ b; simp [h, max]
id                           └─┘
src     └───────┘    └────┘ └┘└─┘└─
typ     └───────┘  └────┘└┘└─┘└─
doc     └───────┘     └────┘ └┘   └─
txt     └───────┘     └────┘ └┘   └─
par     └───────┘     └────┘ └┘   └─
pid                       └┘   
st     └──────────────────────────────
254  
src  
typ  
doc  
txt  
par  
pid  
st   
255  @[simp, move_cast] theorem cast_abs [discrete_linear_ordered_field α] {q : ℚ} :
id                                        └───────────────────────────┘        
src                                       └───────────────────────────┘         
typ                                       └───────────────────────────┘        
doc    └──┘  └───────┘                                                          
256    ((abs q : ℚ) : α) = abs q :=
id       └─┘           └─┘ 
src      └─┘             └─┘
typ      └─┘           └─┘ 
doc              
257  by simp [abs]
id            └─┘
src     └────┘└─┘└─
typ     └────┘└─┘└─
doc     └────┘   └─
txt     └────┘   └─
par     └────┘   └─
pid            
st     └───────────
258  
src  
typ  
doc  
txt  
par  
pid  
st   
259  end rat